(declare-fun r () (Array (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))) (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool)))))))))
(declare-fun var () (Array (Array (Array (Array Int Bool) Bool) (Array (Array (Array Int (Array Int Int)) (Array Int Int)) (Array (Array Int (Array Int Int)) (Array Int Int)))) (Array (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))) (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))))))
(declare-fun r7 () Int)
(declare-fun r76 () (Array (Array Int Bool) Bool))
(declare-fun v () (Array (Array (Array Int Bool) Bool) (Array (Array (Array Int (Array Int Int)) (Array Int Int)) (Array (Array Int (Array Int Int)) (Array Int Int)))))
(declare-fun va () (Array Int Bool))
(declare-fun ar () Int)
(declare-fun a () (Array (Array Int Bool) Bool))
(assert (forall ((ar7 Int) (r9 Int) (r2 (Array (Array (Array (Array Int Bool) Bool) (Array (Array (Array Int (Array Int Int)) (Array Int Int)) (Array (Array Int (Array Int Int)) (Array Int Int)))) (Array (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))) (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))))))) (xor (= r7 ar) (= r76 a) (= r9 0) (and (= var r2) (= r2 (store r2 v r))) (select va 1) (<= r9 0) (= r9 ar7))))
(check-sat)
